Proof-Carrying Code
Proof-Carrying Code (PCC) is a technique where code is distributed with a formal proof that it meets a predefined safety policy. Before execution, the code consumer verifies this proof instead of the safety policy itself. If the proof is correct, the code is considered safe to run. PCC allows safe execution of untrusted code without relying on runtime checks or trusting the code’s source.
Goals
In this seminar, you will become familiar with the fundamental concepts of proof-carrying code. You will also understand how verifiers can be designed to be trustworthy and reliable. Additionally, you will learn how the idea has lately been re-discovered in the field of AI code generation and how it could be leveraged to increase trust in generated code.